E:Type, pred?:(E(E+Unit)), n:, a, j:E.
first(j)  rel_exp(E;x,y. first(y) & x = pred(y)  E;n)(a,j)  a = j 

latex

Definitions

b, P  Q, x:A. B(x), A & B, a<b, P & Q, x f y, rel_exp(T;R;n), x.A(x), A, first(e), s = t, pred(e), n-m, x:A. B(x), P  Q, f(a), "$token", outl(x), if a=b c ; d fi, i=j, Y, isl(x), Case b of inl(x)  s(x) ; inr(y)  t(y), if b t else f fi, b, , t  T, Unit, left+right, x:AB(x), <a,b>, False, x:AB(x), #$n, AB, -n, n+m, Void, {x:A| B(x) }, , Type, Prop, , P  Q, ij, True, T, true, {T}, SQType(T), s ~ t, P  Q

Lemmas

bool sq, assert elim, squash wf, true wf, ge wf, nat properties, unit wf, nat wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bool wf, bnot wf, rel exp wf, not wf, pred wf, le wf, assert wf, first wf